
import types, copy

class all(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, all):
            return self.name == other.name
        else:
            return False
        
    def __repr__(self):
        return self.name

    def __iter__(self):
        return iter([])

class exist(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, exist):
            return self.name == other.name
        else:
            return False
        
    def __repr__(self):
        return self.name

    def __iter__(self):
        return iter([])

class variable(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, variable):
            return self.name == other.name
        else:
            return False
        
    def __repr__(self):
        return self.name

    def __iter__(self):
        return iter([])

class constant(object):
    def __init__(self, content):
        self.content = content
        self.name=content
    def __eq__(self, other):
        if isinstance(other, constant):
            return self.content == other.content
        else:
            return False
        
    def __iter__(self):
        return iter([])
    
    def __repr__(self):
        return self.content

class function(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, function):
            return self.name == other.name
        else:
            return False
    
    def __repr__(self):
        return self.name
    
    def __iter__(self):
        return iter([])

class predicate(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, predicate):
            return self.name == other.name
        else:
            return False
    
    def __repr__(self):
        return self.name
    
    def __iter__(self):
        return iter([])
            
class clause:
    
    def __init__(self):
        #Predicates
        self.P = predicate("P")
        self.Q = predicate("Q")
        self.R = predicate("R")
        self.F = predicate("F")
        
        #Functions
        self.f = function("f")
        
        #Main variables
        self.x = variable("x")
        self.y = variable("y")
        self.z = variable("z")
        
        #Constants
        self.a = constant("a")
        self.b = constant("b")
        self.c = constant("c")
        
        #Renaming Variables
        self.v = variable("v")
        self.u = variable("u")
        self.w = variable("w")
        self.r = variable("r")
        self.s = variable("s")
        self.t = variable("t")
        
        self.A = all("A")
        self.E = exist("E")
        
        self.subVar = [self.u,self.v,self.w,self.x,self.y,self.z]
        self.usedVar=[]
        self.A_var=[]           #variables occurring after a universal quantifier
        self.consts = [self.a,self.b,self.c]
        self.usedConsts = []
        self.existential_exp = []
        self.forAllList = []
        self.sublist_flag = False
        self.final_vars= []
        self.tmp_vars = []
        self.extra_vars = [self.u, self.w, self.t, self.s, self.v, self.r]
        
#        self.s=[self.y,'<=>',self.x]
#        self.s=[self.y,'<=>',[self.x,'=>',self.z]]
#        self.s=[ [self.A,self.y,[self.E,self.x,[[self.P,self.x,self.y],'&',[self.A,self.v,[[self.Q,self.v],'=>','~',[self.P,self.x]]]]]], '&', [self.E,self.z, [self.P,self.z]], '&', [self.E,self.u, [self.P,self.u]] ]
        #self.s=['~',[self.A,self.x,[self.f,self.x]]]
        print '---------------------------------------------------------------------------'
        print 'Test Case 1'
        
        self.s=[self.E,self.x,[[self.P,self.x],'&',[self.A,self.x,[[self.Q,self.x],'=>','~',[self.P,self.x]]]]]
        print 'input = ',self.s
#        self.s = [self.A, self.y, [[self.P, self.y],'<=>',[self.A,self.x,[self.E,self.y,[self.R,self.x,self.y]]]]]
        self.cnf(True)   #trace mood
        print '___________________________________________________________________________'
        self.cnf(False)   #regular mood
        print '---------------------------------------------------------------------------'
        print 'Test Case 2'
        self.s=[self.A,self.x,[[self.P,self.x],'<=>',[[self.Q,self.x],'&',[self.E,self.y,[[self.Q,self.y],'&',[self.R,self.y,self.x]]]]]]
        print 'input = ',self.s
        self.cnf(True)   #trace mood
        print '___________________________________________________________________________'
        self.cnf(False)   #regular mood

    def cnf(self, flag):
        self.subVar = [self.u,self.v,self.w,self.x,self.y,self.z]
        self.usedVar=[]
        self.A_var=[]           #variables occurring after a universal quantifier
        self.consts = [self.a,self.b,self.c]
        self.usedConsts = []
        self.existential_exp = []
        self.forAllList = []
        self.sublist_flag = False
        self.final_vars= []
        self.tmp_vars = []
        if flag == True:
            print 'Trace Mode'
            print '-----------'
            print 'Step1: \n Remove implication <=> '
            self.s=self.resolve(self.s,'<=>')
            print self.s
            print '**************************************'
            print 'Step2: \n Remove implication => '
            self.s=self.resolve(self.s,'=>')
            print self.s
            print '**************************************'
            print 'Step3: \n Push Not Forward:'
            self.s=self.resolve(self.s,'~')
            print self.s
            print '**************************************'
            print 'Step4: \n Standardize apart '
            self.s=self.rename(self.s)
            print self.s
            print '**************************************'
            print 'Step5: \n Skolemize'
            self.remove_E(self.s)
            print self.s
            print '**************************************'
            print 'Step6: \n Discard universal quantifier'
            self.remove_universal(self.s)
            print self.s
            print '**************************************'
            print 'Step7: \n Conjunction of Disjunction'
            self.s=self.conjunction(self.s)
            print self.s
            print '**************************************'
            print 'Step8: \n Flatten Conjunction of Disjunction '
            self.s=self.resolve(self.s,'|')
            self.s=self.resolve(self.s,'&')
            print self.s
            print '**************************************'
            print 'Step9: \n Clause Form'
            self.clause=self.getClause(self.s)
            print self.clause
            print '**************************************'
            self.save_s = copy.deepcopy(self.s)
            print 'Step10: \n Clause with final rename'
            self.s = self.final_rename(self.save_s, 0)
            self.clause=self.getClause(self.s)
            print self.clause
        else:
            print 'Regular Mode'
            print '--------------'
            self.s=self.resolve(self.s,'<=>')
            self.s=self.resolve(self.s,'=>')
            self.s=self.resolve(self.s,'~')
            self.s=self.rename(self.s)
            self.remove_E(self.s)
            self.remove_universal(self.s)
            self.s=self.conjunction(self.s)
            self.s=self.resolve(self.s,'|')
            self.s=self.resolve(self.s,'&')
            self.clause=self.getClause(self.s)
            self.save_s = copy.deepcopy(self.s)
            self.s = self.final_rename(self.save_s, 0)
            self.clause=self.getClause(self.s)
            print 'CNF = ', self.clause
    
    """This method takes as input a list, old & new, where old is what should be replaced in the list 
    & new is what old will be replaced with then it returns the new list with the replacements"""
    def replace_rename(self, list, old, new):
        for i in xrange (0, len(list)): 
            if list[i] == old:
                list[i] = new
            elif isinstance(list[i],types.ListType):
                self.replace_rename(list[i], old, new)
        return list         
    
    """ This method is responsible for doing the standardize apart in the last step
    after clause form, it takes as input a list & an index i then it looks for variables in list[i]
    & checks whether they have already been used in a previous list of disjunctions or not, if they have 
    been used before they become renamed by being replaced with new variables that have not been previously used """
    def final_rename(self, list, i):
        result = []
        for i in xrange(0, len(list)):
            if isinstance(list[i], types.ListType):
                #get all variables in list[i] & store them in tmp_vars
                self.get_all_vars(list[i])
                new_list = list[i]
                for v in self.tmp_vars:
                    if not v in self.final_vars:
                        #variable not used before
                        self.final_vars.append(v)
                     #variable used before & will be replaced
                    else:
                        #make a copy of list to be replaced
                        old_list = copy.deepcopy(list[i])
                        new = self.extra_vars.pop()
                        #replace old list with new list (rename variables)
                        new_list = self.replace_rename(old_list, v, new)
                        self.final_vars.append(new)
                self.tmp_vars = []
                result.append(new_list)
            #list[i] is not a list (probably an operator)
            else:
                result.append(list[i])
        return result
                        
    def oneContainsList(self,list):
        if isinstance(list,types.ListType) and ('&' in list or '|' in list):
            theIn = '&'
            if '&' in list:
                theIn = '&'
            elif '|' in list:
                theIn = '|'
            for m in xrange(0,len(list)):
                if isinstance(list[m],types.ListType):
                    for n in xrange(0,len(list[m])):
                        if isinstance(list[m][n],types.ListType):
                            if '&' in list[m] and not theIn == '&':
                                return True
                            elif '|' in list[m] and not theIn=='|':
                                return True
        return False
    """
    This method removes the brackets put by notBrackets
    """
    def removeNotBrackets(self,list):
        added = False
        i = 0
        while True:
            if added:
                i = i+1
                added = False
            while i<len(list) and isinstance(list[i],types.ListType) and len(list[i])==1 and isinstance(list[i][0],types.ListType) :
                list[i] = list[i][0]
            if i<len(list) and isinstance(list[i],types.ListType):
                list[i] = self.removeNotBrackets(list[i])
            #substitute the current ith element with the ~ and the i+1 with the element beside it in i+1
            if i<len(list) and isinstance(list[i],types.ListType)  and len(list[i])==2 and list[i][0]=='~':
                list.insert(i, '~')
                list.insert(i+1,list[i+1][1])
                list.pop(i+2)
                added = True
            i = i+1
            if i>=len(list):
                break
        while i<len(list) and isinstance(list[i],types.ListType) and len(list[i])==1 and isinstance(list[i][0],types.ListType) :
                list[i] = list[i][0]
        return list
    
    """
    This method adds brackets around the not and the element beside it
    """    
    def notBrackets(self,list):
        popped = False
        for i in xrange(0,len(list)):
            if popped:
                i=i-1
                popped = False
            while i<len(list) and isinstance(list[i],types.ListType) and len(list[i])==1 and isinstance(list[i][0],types.ListType) :
                list[i] = list[i][0]
            if i<len(list) and isinstance(list[i],types.ListType) and len(list[i])>2:
                list[i] = self.notBrackets(list[i])
            #substitute the ~ with brackets around the not and the element beside it
            #and remove the element after it which is the element identical to the 
            #one with the ~
            if i<len(list) and list[i]=='~' and i+1<len(list):
                list[i]=[list[i:i+2]]
                list.pop(i+1)
                popped = True
        for i in xrange(0,len(list)):
            while isinstance(list[i],types.ListType) and isinstance(list[i][0],types.ListType) and len(list[i])==1:
                    list[i] = list[i][0]
        return list
    
    """
    put brackets around the ands to deal with them as one list
    """
    def andBrackets(self,list):
        
        toStartIndex = -1
        toEndIndex = -1
        i = 0
        #it works by finding the index of the start and end of the sublist that should be created
        while True:
            while i<len(list) and isinstance(list[i],types.ListType) and isinstance(list[i][0],types.ListType) and len(list[i])==1:
                list[i] = list[i][0]
            if i<len(list) and isinstance(list[i],types.ListType) and '&' in list[i] and len(list[i])>3:
                list[i] = self.andBrackets(list[i])[0]
            if i<len(list) and list[i] == '&' and toStartIndex == -1:
                toStartIndex = i-1
            elif i == len(list)-1 and not toStartIndex == -1:
                toEndIndex = len(list)
            elif i<len(list) and list[i]=='|' :
                toEndIndex = i-1
                if toStartIndex == -1:
                    toStartIndex = i-1
                    toEndIndex = i-1
            if i<len(list) and toStartIndex == toEndIndex and not toStartIndex == -1:
                list[toStartIndex] = list[toStartIndex]
                toStartIndex = -1
                toEndIndex = -1
            elif i<len(list) and not toStartIndex == -1 and not toEndIndex == -1 and len(list)>3:
                list[toStartIndex] = [list[toStartIndex:toEndIndex]]

                popped = False
                numberOfPopped = 0
                for j in xrange(toStartIndex+1,toEndIndex):
                    if popped:
                        j = j-1
                        popped = False
                    if j<len(list):
                        numberOfPopped = numberOfPopped + 1
                        list.pop(j)
                        popped = True
                if numberOfPopped >2:
                    list.pop()
                toStartIndex = -1
                toEndIndex = -1
            i = i+1
            if i>=len(list):
                break
        for i in xrange(0,len(list)):
            while i<len(list) and isinstance(list[i],types.ListType) and len(list[i])==1 and isinstance(list[i][0],types.ListType) :
                    list[i] = list[i][0]
        return list
    
    """
    This is the method used to apply the following rules 
                x&x = x
                x | (x&y) = x
                x & (x|y) = x
    and calling findCon when supposed to on the required parts
    """
    def conjunction(self,passed):
        list = []
        for i in passed:
            list.append(i)
        #print 'WITHOUT not brackets',list
        #first we need to have brackets around the not variables to have both considered as one in the swaping operations
        list = self.notBrackets(list)
        prevList = list#if this prevList does not change in a certain loop, then no more changes can be done and can exit
        #print 'list with not brackets',list
        
        #put brackets around the anded terms
        list = self.andBrackets(list)
        #print 'WITH and brackets',list
        
        #loop loops until we can no more change the list
        while True:
            prevList = list
            #remove unneccassary brackets around the list
            while len(list)==1 and isinstance(list[0],types.ListType):
                list = list[0]
            for i in xrange(0,len(list)):
                #if list[i] == '|' or '&' then we should compare the element before it with elements ahead 
                #and according to these rules the algorithm works:
                # x&x = x
                # x | (x&y) = x
                # x & (x|y) = x
                if i<len(list) and list[i] == '|':
                    jIndex = 0
                    for j in xrange(i+1,len(list)):
                        if j<len(list) and list[j] == '|' and not i==j:
                            jIndex = j-1
                        elif j+1 == len(list) and list[j-1] == '|':
                            jIndex = j
                        if( (list[j] == '|' and not i==j) or (j+1 == len(list) and list[j-1] == '|' )):
                            if list[i-1] == list[jIndex] and not jIndex == i-1:
                                #if they're equal remove
                                list.pop(j)
                                list.pop(j-1)
                                if i>j:
                                    i = i-2
                                j = j-2
                                i = i-1
                            elif list[i-1] in list[jIndex]:
                                #if one contains the other then one is discarded
                                if '&' in list[jIndex] and not '|' in list[jIndex]:
                                    list.pop(j)
                                    list.pop(j-1)
                                    if i>j:
                                        i = i-2
                                    j = j-2
                                    i = i-1
                                elif '|' in list[jIndex] and not '&' in list[jIndex]:
                                    list.pop(i)
                                    list.pop(i-1)
                                    if j>i:
                                        j = j-2
                                    i = i-2
                                    i = i-1
                            elif list[jIndex] in list[i-1]:
                                if '&' in list[i-1] and not '|' in list[i-1]:
                                    list.pop(i)
                                    list.pop(i-1)
                                    if j>i:
                                        j = j-2
                                    i = i-2
                                    i = i-1
                                elif '|' in list[i-1] and not '&' in list[i-1]:
                                    list.pop(j)
                                    list.pop(j-1)
                                    if i>j:
                                        i = i-2
                                    j = j-2
                                    i = i-1
                            else:
                                #this means that its an OR and needs to find the CNF
                                list = self.findCon(list)
                elif i<len(list) and list[i] == '&':
                    #the same checks but opposite that is all '&' are '|' here and all '|' are '&'
                    jIndex = 0
                    for j in xrange(i+1,len(list)):
                        if j<len(list) and list[j] == '&' and not i==j:
                            jIndex = j-1
                        elif j+1 == len(list) and list[j-1] == '&':
                            jIndex = j
                        if ((j<len(list) and list[j] == '&' and not i==j) or (j+1 == len(list) and list[j-1] == '&' )):
                            if list[i-1] == list[jIndex] and not jIndex == i-1:
                                list.pop(j)
                                list.pop(j-1)
                                if i>j:
                                    i = i-2
                                j = j-2
                                i = i-1
                                #print 'checked equality'
                            elif list[i-1] in list[jIndex]:
                                if '|' in list[jIndex] and not '&' in list[jIndex]:
                                    list.pop(j)
                                    list.pop(j-1)
                                    if i>j:
                                        i = i-2
                                    i = i-2
                                    i = i-1
                                elif '&' in list[jIndex] and not '|' in list[jIndex]:
                                    list.pop(i)
                                    list.pop(i-1)
                                    if j>i:
                                        j = j-2
                                    i = i-2
                                    i = i-1
                            elif not isinstance(list[jIndex],types.ListType) and list[jIndex] in list[i-1]:
                                if '|' in list[i-1] and not '&' in list[i-1]:
                                    list.pop(j)
                                    list.pop(j-1)
                                    if i>j:
                                        i = i-2
                                    j = j-2
                                    i = i-1
                                elif '&' in list[i-1] and not '|' in list[i-1]:
                                    list.pop(i)
                                    list.pop(i-1)
                                    if j>i:
                                        j = j-2
                                    i = i-2
                                    i = i-1
                                    #if one of the being compared parts contains a list then 
                                    #recursive call on conjunction on that list
                            elif self.oneContainsList(list[jIndex]):
                                list[jIndex] = self.conjunction(list[jIndex])
                                list = self.flatten(list,'&')
                                if self.oneContainsList(list[i-1]):
                                    prevLength = len(list)
                                    prevJ = j
                                    list[i-1] = self.conjunction(list[i-1])
                                    j = prevJ
                                    #make sure that i and j are decreased with the appropriate amount
                                    #using the preLength of the list before performing 
                                    #the recursive conjunction
                                    if not len(list) == prevLength:
                                        i = i-(prevLength-len(list))
                                        j = j-(prevLength-len(list))
                                    list = self.flatten(list,'&')
                            elif self.oneContainsList(list[i-1]):
                                prevLength = len(list)
                                prevJ = j
                                list[i-1] = self.conjunction(list[i-1])
                                j = prevJ
                                if not len(list) == prevLength:
                                    i = i-(prevLength-len(list))
                                    j = j-(prevLength-len(list))
                                if self.oneContainsList(list[i-1]):
                                    list[i-1] = self.conjunction(list[i-1])
            if list == prevList:
                break
        list = self.removeNotBrackets(list)
        if list[len(list)-1] == '&':
            list.pop()
            if isinstance(list,types.ListType) and len(list)==1:
                list = list[0]
        #remove the not brackets inserted for help at the beginning
        return list
    
    """
    This method calls the conDis which performs the 
    conjunctions of disjunctions on the parameters that should be anded or ored together 
    from the list
    """
    def findCon(self,list):
        result = []
        for i in xrange(0,len(list)):
            if list[i] == '|':
                if '&' in list[i-1]:#this means that the list of ands is at the beginning
                    if isinstance(list[i-1],types.ListType):
                        #then call CNF with list[i+1] the to be or'ed
                        result = self.conDis(list[i+1],list[i-1],'|') 
                if '&' in list[i+1]:#this means that the list of ands is after the or's
                    if isinstance(list[i+1],types.ListType):
                        #then call CNF with list[i-1] the to be or'ed
                        result = self.conDis(list[i-1],list[i+1],'|')
        
        return result   
    
    """
    This method performs the Conjunctions of disjunctions
    """
    def conDis(self,list1,list2,symbol):
        result = []   
        #loop on the second list of or's and or the list1 with the elements to be anded altogether for CNF     
        for e in list2:
            if not e=='&' and symbol == '|':
                #append the first element in the list
                list1_temp = [list1]
                #then the OR
                list1_temp.append('|')
                #then the element to be or'ed with
                list1_temp.append(e)
                #and then bracketize that part
                list1_temp = [list1_temp]
                #and then extend the result with this list
                result.extend(list1_temp)
                result.append('&')
                #not needed in our context but for performing disjunctions of conjunctions
            elif not e =='|' and symbol == '&':
                list1_temp = [list1]
                list1_temp.append('&')
                list1_temp.append(e)
                list1_temp = [list1_temp]
                result.extend(list1_temp)
                result.append('|')
        #remove the unused & at the end
        result.pop()
        return result 
   
    """This method takes as input a list searches recursively in it for any variables then saves them in tmp_vars"""   
    """This method takes as input a list searches recursively in it for any variables then saves them in tmp_vars"""   
    def get_all_vars(self, list):
        for i in xrange(0,len(list)):
            if isinstance(list[i],variable):
                #if list[i] is not already stored in tmp_vars
                if not list[i] in self.tmp_vars:
                    #then store in tmp_vars
                    self.tmp_vars.append(list[i])
            elif isinstance(list[i],types.ListType):
                #keep looking for variables recursively
                self.get_all_vars(list[i])  

    """ This is the method used for flatten OR,AND. 
    It takes as input:
    list: the list to flatten
    symbol: to either flatten the | or & """           
    def flatten(self,list,symbol):
        new=[]
        for i in xrange(0,len(list)):
            if isinstance(list[i],types.ListType) and not isinstance(list[i][0],(predicate,function)):
                # if flatten OR and the element is of type list and not predicate nor function
                # extend that the list in the new list, extend will open the 2 lists on each other
                if symbol == '|':
                    new.extend(list[i])
                else:
                # if flatten AND while the element is of type list and not predicate nor function
                # extend the result from flatten the list
                    new.extend(self.flatten(list[i],symbol))
            # Append the symbol
            elif list[i]==symbol:
                new.append(symbol)
            # If flatten AND, found the symbol OR then put the whole list which contains OR
            # as one of it's elements into a new list and append it to the new list
            # and break from lopping on the rest of the list
            elif list[i]=='|' and symbol=='&':
                new=[]
                new.append(list)
                break
            # Else just append the element 
            else:
                new.append(list[i])
        # return the new list result from the looping
        return new
    
    
    """ This method is responsible from moving the not on the given list
    It takes input : s = which is list we will move the negation on """            
    def move_not_inwards(self,s):
        #The list we store it the new resulted list
        # after performing the transfromation on the old list
        new=[]
        # puts the list in a temp list called a_imp
        a_imp=s
        i=0
        
        #Base Case if it finds a Predicate, Function or variable it just puts the not before them
        # It loops on each element and performs several checks
        while i <len(a_imp):
            
            # If the element is of type list
            # It does checks if it's a predicate or function it just append '~' and the list in the new list
            # Else it appends to new the result from moving not on that list
            if isinstance(a_imp[i],types.ListType):
                if isinstance(a_imp[i][0],(predicate,function)):
                    new.append('~')
                    new.append(a_imp[i])
                else:
                    new.append(self.move_not_inwards(a_imp[i]))   
            # If the list is of type forAll it appends the thereExist and the variable
            # else the list is of type thereExist it appends the forAll and the variable
            #and continues looping on the element after skipping the variable       
            elif(isinstance(a_imp[i],exist)):
                new.append(self.A)
                new.append(a_imp[i+1])
                i=i+1
            elif(isinstance(a_imp[i],all)):
                new.append(self.E)
                new.append(a_imp[i+1])
                i=i+1
            # If it's a symbol | or & just append the symbol
            elif a_imp[i]=='&':
                new.append('|')
            elif a_imp[i]=='|':
                new.append('&')
            # if the element is ~ it skips it to the element after it
            # and appends the element after it
            elif a_imp[i]=='~':
                new.append(a_imp[i+1])
                i=i+1
            else:
                new.append('~')
                new.append(a_imp[i])
            i=i+1            
        return new
    
    """ This is the method responsible of eliminating both implications and
    replacing it with the equivalent rule
    It takes as input the 
    -list s: which perform the elimination function on
    This function will contain the symbol we want to replace
    - symbol: which will say whether we are performing <=> or => elimination
    """ 
    def eliminate_implications(self,s,symbol):

        b_imp=[]
        a_imp=[]

        # the for loop is used to split the list into 2 lists
        # b_imp the part of the list before the symbol
        # a_imp the part of the list after the symbol
        # both a_imp and b_imp doesn't include the symbol
        # Example: s= (A => B) this loop will give us b_imp=[A], a_imp=[B]
        for i in xrange(0,len(s)):
            if s[i] == symbol:
                b_imp=s[:i]
                a_imp=s[i+1:]

        # if before and after lists are empty therefore the list given
        # doesn't contain the symbol so set new to empty list
        # and loop on the input list to do recursive eliminate implicaiton 
        # incase the given lisy consists of a list with a sublist containing the symbol
        if a_imp == [] and b_imp==[]:
            new=[]
            for b in s:
                if isinstance(b,types.ListType):
                    if isinstance(b[0],(predicate,function) ):
                        new.append(b)
                    else:
                        new.append(self.eliminate_implications(b,symbol))
                else:
                    new.append(b)
            return new
        
        if symbol=='=>':
        # It will append ~ then loop on the b_imp and append element by element 
        # and if the element is a list it will call eliminate implication on this list
        # after done with b_imp will append | and finally loop on a_imp and perform as done
        #on b_imp
            new = ['~']
            for b in b_imp:
                if isinstance(b,types.ListType):
                    if isinstance(b[0],(predicate,function) ):
                        new.append(b)
                    else:
                        new.append(self.eliminate_implications(b,symbol))
                else:
                    new.append(b)
            new.append('|')
            for a in a_imp:
                if isinstance(a,types.ListType):
                    if isinstance(a[0],(predicate,function) ):
                        new.append(a)
                    else:
                        new.append(self.eliminate_implications(a,symbol))
                else:
                    new.append(a)
        elif symbol=='<=>':
            #Example: s=[A <=> B]
            # new1 = [A => B]
            # new2 = [B => A]
            # new = [new1 & new1]
            
            
            # new is the final list to be returned
            new=[]
            
            # new1 is the list containing the first half of removing <=>
            # which is b_imp => a_imp
            new1=[]
            # new1 and new2 are filled in the same way difference is the
            # order who is looped on first
            
            for b in b_imp:
            # loop on all the elements if it's of type list and not of type predicate or function
            # it will call eliminate_implication on that list else just append
                if isinstance(b,types.ListType):
                    if isinstance(b[0],(predicate,function) ):
                        new1.append(b)
                    else:
                        new1.append(self.eliminate_implications(b,symbol))              
                else:
                    new1.append(b)
            new1.append('=>')
            for a in a_imp:
                if isinstance(a,types.ListType):
                    if isinstance(a[0],(predicate,function) ):
                        new1.append(a)
                    else:
                        new1.append(self.eliminate_implications(a,symbol))
                else:
                    new1.append(a)
            new.append(new1)
            new.append('&')
            
            # new2 is the list containing the second half of removing <=>
            # which is a_imp => b_imp
            new2=[]
            for a in a_imp:
                if isinstance(a,types.ListType):
                    if isinstance(a[0],(predicate,function) ):
                        new2.append(a)
                    else:
                        new2.append(self.eliminate_implications(a,symbol))
                else:
                    new2.append(a)
            new2.append('=>')
            for b in b_imp:
                if isinstance(b,types.ListType):
                    if isinstance(b[0],(predicate,function) ):
                        new2.append(b)
                    else:
                        new2.append(self.eliminate_implications(b,symbol))
                else:
                    new2.append(b)
            new.append(new2)
        else:
            new=s
            

        return new

    """ This method is responsible of replacing all occurrences of a specific
     variable with another one in a specific list
     The method takes several inputs:
     - list : the list will replace in 
     - oldVar : the variable to be replaced
     - newVar : the variable to replace the old one with
     """    
    def renameVar(self,list,oldVar,newVar):

        new=[]
        # loop on the list if finds a variable and is equal to the oldVar entered
        # will append the newVar else just append in the new list
        # if the element is of type list loop recursively
        for l in xrange(0,len(list)):
            if isinstance(list[l],variable) and list[l]==oldVar:
                new.append(newVar)
            elif isinstance(list[l],types.ListType):
                temp=self.renameVar(list[l],oldVar,newVar)
                # Extra check incase there is a unifier to be renamed in the list
                # We are renaming it's vars
                if isinstance(list[l][0],(exist,all)):
                    if list[l][1] in self.usedVar:
                        sub=self.subVar.pop()
                        
                        self.usedVar.append(sub)
                        new.append(self.renameVar(temp,list[l][1],sub))
                    else:
                        if list[l][1] in self.subVar:
                            self.subVar.remove(list[l][1])
                        self.usedVar.append(list[l][1])
                else:        
                    new.append(temp)
            else:
                new.append(list[l])

        return new

    """ This method is responsible of replacing all occurrences of a specific
     list with another one in a the list consisting the list to be replaced
     The method takes several inputs:
     - l : old list to be replaced 
     - y : new list to replace with
     - s : the list the replacement occurs in 
    """
    def search_replace(self,l,y,s):
        #Checks if the list itself is the equal to the old to be replaced
        # then the whole list to the new one
        if s == l:
            s=y
        else:
        # loop on all the elements of the big list s 
        # and every time we find the old list to be replaced we replace it with the new one
        # but if the element is of type list call the search_replace recursively on it
        # incase the old list occurs in a sublist of the main list
            for i in xrange(0,len(s)):
                if s[i] == l:
                    s[i]=y
                elif isinstance(s[i], types.ListType):
                    self.search_replace(l,y,s[i])
        return s
    
    """This method is responsible of detecting if there is the same variable
    used more than once with different quantifiers"""            
    def rename(self,list):

        for l in xrange(0,len(list)):
            # It loops on every element of the list if the element is of type list call
            # method rename recursively on the that list
            if isinstance(list[l], types.ListType):

                self.rename(list[l])
            # If it detects one of the quantifiers, it checks if the variable
            # is previously taken by a previously mentioned quantifiers
            # we keep track of the variables used in a global list called usedVar
            elif isinstance(list[l],(exist,all)):
                
                if list[l+1] in self.usedVar:
                    # if the variable is used then it is replaced with a variable not 
                    # used before from the list called subVar
                    # and after replacing this variable is poped of the subVar list
                    # and added to the usedVar list
                    temp=self.subVar.pop()                    
                    self.usedVar.append(temp)
                    # and calls the renameVar to perform the renaming in all the list
                    new = self.renameVar(list,list[l+1],temp)

                    return self.search_replace(list,new,self.s)
                else:
                    # extra check incase the variable of the quantifier is
                    # available in the subVar list then it is removed from the subVar
                    if list[l+1] in self.subVar:
                        self.subVar.remove(list[l+1])
                        
                    self.usedVar.append(list[l+1])
        return list 
    
    """This method takes a list and a symbol we want to resolve on
    It keep on looping recursively on all the list and the sub-lists
    and once it finds a list consisting of the symbol given to the function 
    it calls the corresponding method to that condition.
    The result returned from that function is then given to the replace method """
    def resolve(self,list,symbol):

        for l in xrange(0,len(list)):
            if isinstance(list[l], types.ListType):
                self.resolve(list[l],symbol)
            elif list[l] == symbol:

                if symbol == '=>' or symbol == '<=>':
                    new=self.eliminate_implications(list,symbol)
                    return self.search_replace(list,new,self.s)
                
                if symbol == '~' :
                    if isinstance(list[l+1],types.ListType):
                        if not isinstance(list[l+1][0],(function,predicate)):
                            new=self.move_not_inwards(list[l+1])
                    
                            old=list
                            old.remove(list[l+1])
                            old.insert(l+1,new)
                            old.pop(l)
                            return self.search_replace(list,old,self.s)
                            
                if symbol == '|' or symbol == '&':
                    new=self.flatten(list,symbol)
                    return self.search_replace(list,new,self.s)
        
        return list  
    
    """This method takes as input a list & removes from it the universal quantifiers"""   
    def remove_universal(self, s):
        for i in xrange(0,len(s)):
            if isinstance(s[i],all):
                #print s[i], 'all'
                self.s = self.search_replace(s, s[i+2], self.s)
                self.remove_universal(self.s)
            elif isinstance(s[i], types.ListType):
                self.remove_universal(s[i])
        
   
    """This method store variables coming after universal quantifiers in self.A_var then 
    calls remove_E which removes existential quantifiers & replaces them with functions of
    universal variables (stored in self.A_var) or constants in case an existential quantifier 
    is found or it keeps looking for more universal quantifiers to store their variables """
    def getUniversalVars(self, list):
        if isinstance(list[0], (all)):
            #found universal quantifier
            self.A_var.append(list[1])
            #look for nested universal quantifiers
            self.getUniversalVars(list[2:][0])
            #if there's an existential quantifier after a universal one
        elif isinstance(list[0], (exist)):
            #remove existential quantifier
            self.remove_E(list)
    
    """This method takes as input two lists & return true if the 
    first list is an ancestor of the second one"""   
    def sublist(self, parent, list):
        for i in parent:
            if list == i:
                self.sublist_flag = True
            elif isinstance(i, types.ListType):   
                self.sublist(i, list)
    
    """This method removes existential quantifiers & replaces their variables 
    with functions of constants or universal quantifiers' variables"""                
    def remove_E(self, list):
        character = ''
        exp1 = []
        exp2 = []
        for l in xrange(0,len(list)):
            #universal quantifier followed by character, followed by list
            if isinstance(list[l], all) and isinstance(list[l+1], variable) and isinstance(list[l+2], types.ListType):     
                self.forAllList = list
                #save universal quantifier variable in self.A
                if not list[l+1] in self.A_var:
                    self.A_var.append(list[l+1])
                #call remove_E recursively again to look for existential quantifiers
                self.remove_E(list[l+2])
            #universal quantifier followed by character, followed by not, followed by list
            elif isinstance(list[l], all) and isinstance(list[l+1], variable) and list[l+2] =='~' and isinstance(list[l+3], types.ListType):     #exist followed by character, followed by list
                self.forAllList = list
                if not list[l+1] in self.A_var:
                    self.A_var.append(list[l+1])
                #call remove_E recursively again to look for existential quantifiers
                self.remove_E(list[l+3])    
            #existential quantifier followed by character, followed by list
            elif isinstance(list[l], exist) and isinstance(list[l+1], variable) and isinstance(list[l+2], types.ListType):     #exist followed by character, followed by list
                character = list[l+1]
                self.existential_exp = list[l+2]  
                exp1 = [list[l], list[l+1], list[l+2]]
                exp2 = self.existential_exp
                tmp = []
                tmp.append(self.F)
                self.sublist(self.forAllList, list)
                #check if we have existential inside universal quantifier
                if self.sublist_flag == True:
                    tmp.extend(self.A_var)
                else:
                    #construct function of constants
                    for t in self.consts:
                        if not t in self.usedConsts:
                            tmp.append(t)
                            self.usedConsts.append(t)
                            break
                self.sublist_flag = False    
                #replace exp1 with exp2 to get the new function
                self.s = self.search_replace(exp1, exp2, self.s)
                self.s = self.search_replace(character, tmp, self.s)
                self.A_var = []
                self.remove_E(self.s)
            #existential quantifier followed by character, followed by not,  followed by list
            elif isinstance(list[l], exist) and isinstance(list[l+1], variable) and list[l+2] == '~' and  isinstance(list[l+3], types.ListType):     #exist followed by character, followed by list
                #print 'found there exist', list
                character = list[l+1]
                self.existential_exp = [list[l+2], list[l+3]]
                exp1 = [list[l], list[l+1], list[l+2], list[l+3]]
                exp2 = self.existential_exp
                tmp = []
                tmp.append(self.F)
                self.sublist(self.forAllList, list)
                #check if we have existential inside universal quantifier
                if self.sublist_flag == True:
                    tmp.extend(self.A_var)
                else:
                    #construct function of constants
                    for t in self.consts:
                        if not t in self.usedConsts:
                            tmp.append(t)
                            self.usedConsts.append(t)
                            break
                self.sublist_flag = False    
                #replace exp1 with exp2 to get the new function
                self.s = self.search_replace(exp1, exp2, self.s)
                self.s = self.search_replace(character, tmp, self.s)
                self.A_var = []
                self.remove_E(self.s)
            elif isinstance(list[l], types.ListType):
                self.remove_E(list[l])                   
    
    """This method convert the list look of the predicate or function to the readable form.
    Example if given list = [P,x] it returns P(x) as a string. """
    def changelook(self,list):
        new=''
        for j in list:
            if isinstance(j,(predicate,function)):
                new+=j.name
                new+='('
            elif isinstance(j, types.ListType):
                new+=self.changelook(j)
            else:
                new+=j.name
                new+=','
        new=new[:-1]
        new+='),'
        return new
    
    """This method is responsible of converting the list given as input into
    it's equivalent clause form """    
    def getClause(self,list):
        # Initially it adds the start bracket of the list
        new='{'
        
        for i in xrange(0,len(list)):
        # Loops on every element of the list
        # if the element is of type list then check if they are
        # of type predicate or function then append the result of
        # changelook on this list
        # else call the method getClause recursively on that list
            if isinstance(list[i],types.ListType):
                if isinstance(list[i][0],(predicate,function)):
                    # This is an extra check to avoid not putting brackets around the predicate
                    # if the predicate is not ored and it is anded with something else
                    a=False
                    if i<=len(list)-2:
                        if(list[i+1]=='|'):
                            a=True
                    elif i>=2:
                        if list[i-1]=='|' or list[i-2]=='|':
                            a=True
                    temp=self.changelook(list[i])
                    if not a:
                        new+='{'
                        new+=temp[:-1]
                        new+='}'
                    else:
                        new+=temp[:-1]
                    
                else:
                    new+=(self.getClause(list[i]))
            # if the element is of symbol | or & then append , 
            elif list[i]=='|' or  list[i]=='&':
                new+=','
            # else just append the element
            else:
                new+=list[i]
        # After breaking of the loop add a closing bracket to the end of the list        
        new+='}'
        
        return new            
    
if __name__ == "__main__":
    clause()
